Nuprl Lemma : strongwf-monotone
11,40
postcript
pdf
T
:Type,
R1
,
R2
:(
T
T
Type).
rel_implies(
T
;
R2
;
R1
)
SWellFounded(
R1
(
x
,
y
))
SWellFounded(
R2
(
x
,
y
))
latex
Definitions
x
(
s1
,
s2
)
,
x
f
y
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
rel_implies(
T
;
R1
;
R2
)
,
x
:
A
B
(
x
)
,
a
<
b
,
f
(
a
)
,
,
{
x
:
A
|
B
(
x
)}
,
Type
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
SWellFounded(
R
(
x
;
y
))
,
x
,
y
.
t
(
x
;
y
)
Lemmas
strongwellfounded
wf
,
rel
implies
wf
,
nat
wf
origin
T:Type, R1,R2:(T
TType).
SWellFounded(R1(x,y)) SWellFounded(R2(x,y)) T:Type, R1,R2:(TTType).
SWellFounded(R1(x,y)) SWellFounded(R2(x,y)) 
T Qx:A. B(x)B(x)
x:A. B(x)
B(x)
x,y. t(x;y)